1. Field
The present invention relates generally to functional verification of circuit designs and, more particularly, to synthesis techniques used in constructing logic networks used in the functional verification process.
2. Description of the Related Art
Today, integrated circuits (ICs) typically contain large numbers of circuit elements. Computer-aided design (CAD) and computer-aided engineering (CAE) tools are essential in assisting circuit designers to produce these complicated ICs. Circuit designs are typically represented in a user-specified hardware description language (HDL), which demonstrate the functional properties of the circuit.
Designers commonly utilize CAE software to translate a HDL representation, which is typically in Register-Transfer-Level (RTL) description, into a gate-level netlist representation, and perform design validation to ensure that no design errors occurred in the process. With increasing design complexity, formal verification (equivalence checking) becomes integral in the design process to ensure that a refinement of the original specification (commonly referred to as revised circuit or design) is equivalent to the original specification (commonly referred to as golden circuit or design).
Conventional verification methods utilize Binary Decision Diagrams (BDDs) to represent the logic circuits involved in equivalence relationships. A primary drawback to using BDDs is their exponential memory complexity associated with large complex designs. The exponential memory complexity associated with using BDDs limits its applicability.
Various methods that attempt to address the deficiencies inherent in using BDDs have been presented. (See e.g., J. Jain, R. Mukherjee, and M. Fujita, Advanced Verification Techniques Based on Learning, Proc. 32nd ACM/IEEE DAC, Jun. 1995, 420-26; W. Kunz, HANNIBAL: An Efficient Tool for Logic Verification Based on Recursive Learning, Proc. 1993 IEEE Intl. Conf. On CAD, November 1993, 538-43; Y. Matstunaga, An Efficient Equivalence Checker for Combinatorial Circuits, Proc. 33rd ACM/IEEE DAC, June 1996, 629-34; A. Kuehlmann, F. Krohm, Equivalence Checking Using Cuts and Heaps, Proc. Intl. Conf. Computer-Aided Design, 1997).
These techniques rely on the existence of intermediate functions that occur in the specification and in the implementation of the circuit design. The intermediate functions are utilized as cut points to partition a complex circuit network into a set of smaller and simpler comparisons. In general, there is a correlation between the number of cut points and equivalence checking performance. Therefore, it is preferable to create a golden circuit that is synthesized to have high structural similarity to the revised circuit to increase the possibility of obtaining more cut points. However, the aforementioned techniques fail to address generating golden circuits having a high number of cut points.
Thus, systems and methods for creating a golden circuit having high structural similarity to the revised circuit is desired. Verification systems incorporating synthesis methods that allow it to efficiently determine the architecture of a revised circuit, and subsequently use that knowledge to construct logic networks having an architecture closely resembling the revised circuit is also desired.
The present invention provides a system and corresponding methods for enhancing the capability of verifying functional equivalence of circuits. The system and methods identify and uncover an underlying architecture of a revised circuit, and uses the extracted information to construct logic networks having an architecture that closely resembles the architecture of the revised circuit. The logic networks can be used to create a golden circuit having enhanced similarity to the revised circuit.
For purposes of summarizing the invention, certain aspects, advantages, and novel features of the invention have been described herein. It is to be understood that not necessarily all such advantages may be achieved in accordance with any one particular embodiment of the invention. Thus, the invention may be embodied or carried out in a manner that achieves or optimizes one advantage or group of advantages as taught herein without necessarily achieving other advantages as may be taught or suggested herein.
In one embodiment, a method for modeling a circuit design includes: synthesizing a circuit design to create a first gate-level representation of the circuit design, analyzing a second gate-level representation of the circuit design to learn architecture information; and resynthesizing the first gate-level representation of the circuit design to incorporate the learned architecture information from the second gate-level representation of the circuit design.
In another embodiment, analyzing a second gate-level representation of the circuit design includes: identifying a first subcircuit in a first gate-level representation of the circuit design; identifying a second subcircuit in the second gate-level representation of the circuit design, the second subcircuit corresponding to the first subcircuit; and calculating a similarity between the first subcircuit and the second subcircuit.
In still another embodiment, a computer-readable storage medium has stored thereon computer instructions that, when executed by a computer, cause the computer to: synthesize a circuit design to create a first gate-level representation of the circuit design; analyze a second gate-level representation of the circuit design to learn architecture information; and resynthesize the first gate-level representation of the circuit design to incorporate the learned architecture information from the second gate-level representation of the circuit design.
In yet another embodiment, a computer-readable storage medium has stored thereon computer instructions that, when executed by a computer, cause the computer to: identify a first subcircuit in a first gate-level representation of a circuit design; identify a second subcircuit in a second gate-level representation of the circuit design, the second subcircuit corresponding to the first subcircuit; and calculate a similarity between the first subcircuit and the second subcircuit.
A technical advantage of the present invention includes providing a design verification system and method that synthesizes a circuit design to create a first gate-level representation of the circuit design. The design verification system then extracts logic network information from a second representation of a circuit design. The extracted information is then used to resynthesize the first representation of the circuit design. Thus, the first representation is created to have logic network architecture and structure that is similar to that contained in the first representation. The similar logic architecture and structure provides increased efficiency in performing functional equivalence verification between the first and second representation of the circuit design.
These and other embodiments of the present invention will also become readily apparent to those skilled in the art from the following detailed description of the embodiments having reference to the attached figures, the invention not being limited to any particular embodiment(s) disclosed.